(declare-fun x0 () Real)
(declare-fun x1 () Real)
(declare-fun x2 () Real)
(declare-fun x3 () Real)
(declare-fun x4 () Real)
(assert (or (= (+ (* 24 x2) (* 21 x1)) (- 25)) (not (< (+ (* (- 42) x2) (* 19 x2) (* (- 48) x1) (* 37 x0)) 38))))
(assert (< (+ (* (- 40) x2) (* x3) (* (- 30) x4) (* (- 45) x2) (* 39 x3)) 0))
(assert (or (not (> (+ (* x0) (* (- 42) x1) (* (- 5) x4) (/ 13 x1) (* (- 49) x4)) 0)) (not (<= (+ (* (* 3 23) x2) (* (- 35) x3)) 37)) (not (<= (+ (* x2)) 10))))
(assert (>= (+ (* 38 x0) (* 6 x1) (* (- 48) x1) (* (- 27) x4) (* (- 14) x2) (* 40 x4) (* 26 x3)) 42))
(push)
(pop)
(assert (or (<= (+ (* 30 x1) (* 41 x2) (* (- 37) x1)) 0) (< (+ (* x0) (* (div 53 1) x2) (* 79 x1) (/ (- 47) x0) (* (- 22) x4) (* 49 x0) (* x1) 0) 19)))
(check-sat)
(assert (not (> (+ (* (- 44) x3) (* (- 46) x4) 0 (* 26 x3) (* (- 27) x4) (* 26 x4) (* 21 x4) (* 44 x0) 0) (- 41))))
(assert (or (not (< (+ (* 22 x2) (* (- 64) x0)) (- 28))) (<= (+ (* 41 x1) (* 7 x4)) (- 10))))
(assert (not (<= (+ (* (- 21) x2) (* (- 6) x3) (* (- 24) x3) (* (- 17) x1) (* (- 31 5) x0)) (- 124))))
(assert (or (< (+ (* 16 x2) (* 48 x3) (* 20 x2) (* 15 x0) (* (- 33) x0)) 44) (not (<= (+ (* (- 46) x4) (* x0) (* (- 27) x0) (* (- 11) x4) (* (- 32) x0) (* x3) (* (- 25) x1)) 0))))
(check-sat)
(check-sat)
(assert (or (not (< (+ (* (- 5) x2) (* (- 22) x3) (* 2 x0) (* 42 x1) (* 12 x3) (* 16 x3) (* (- 19) x0) (* (- 42) x0) (* (- 6) x1)) 40)) (> (+ (* 7 x0) (* 9 x1) (* 14 x2) (* 4) (* (- 16) x3) (* 41 x1)) 0)))
(assert (or (= (+ (* (- 36) x4) 0) (- 16)) (< (+ (* (- 10) x1) (* 39 x4) (* (- 47) x3) (* (- 39) x0) (* 24 x2) (* 24 x1)) (- 21))))
(check-sat)
(assert (or (< (+ (* (- 7) x3) (* 35 x2) (* (- 42) x1) (* 43 x3) (* 27 x3) (* (- 47) x2) (* (- 5) x2) (* 13 x0) (* 36 x4)) (- 38)) (not (<= (+ (* 36 x0) (* 46 x2) (* (- 9) x2) (* 4 x1) (* x3) (* 0 x2) (* (- 19) x3) (* (- 25) x3)) 0))))
(assert (or (= 0 (- 38)) (< (div (* 13 x2) (* (- 44) x3) (* 12 x2) (* (- 6) x2) (* 25 x2)) (- 50))))
(assert (or (not (= (+ (* x1)) (- 13))) (= (+ (* x3) (* x0)) 0)))
(check-sat)
